es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p, p':({e:E| loc(e) = loc(e1)  Id }Prop).
(e:{e:E| loc(e) = loc(e1)  Id }. p(e)  p'(e))
 (e2 = first e  e1.p(e)  e2 = first e  e1.p'(e)) 

latex

Definitions	x(s), t  T, b, P  Q, False, A, x:A. B(x), P & Q, P  Q, (e <loc e'), loc(e), Id, E, P  Q, e  e' , e[e1,e2).P(e), e2 = first e  e1.P(e), ES, Prop, x. t(x)
Lemmas	es-first-since wf, iff wf, event system wf, es-E wf, es-le wf, es-locl wf, Id wf, es-loc wf, es-le-loc, es-loc-pred, es-locl-iff